0 Prolog
↳1 PrologToPiTRSProof (⇒, 0 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 89 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 5 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇒, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 PiDP
↳22 UsableRulesProof (⇔, 0 ms)
↳23 PiDP
↳24 PiDPToQDPProof (⇒, 0 ms)
↳25 QDP
↳26 MRRProof (⇔, 9 ms)
↳27 QDP
↳28 PisEmptyProof (⇔, 0 ms)
↳29 YES
palindrome_in_g(L) → U1_g(L, halves_in_gaaa(L, X1s, X2s, EvenOdd))
halves_in_gaaa([], [], [], even) → halves_out_gaaa([], [], [], even)
halves_in_gaaa(.(X, []), .(X, []), [], odd) → halves_out_gaaa(.(X, []), .(X, []), [], odd)
halves_in_gaaa(.(T, .(Y, Xs)), .(T, Ts), .(R, Rs), EvenOdd) → U6_gaaa(T, Y, Xs, Ts, R, Rs, EvenOdd, last_in_gaa(.(Y, Xs), R, Rests))
last_in_gaa(.(T, []), T, []) → last_out_gaa(.(T, []), T, [])
last_in_gaa(.(H, T), X, .(H, M)) → U8_gaa(H, T, X, M, last_in_gaa(T, X, M))
U8_gaa(H, T, X, M, last_out_gaa(T, X, M)) → last_out_gaa(.(H, T), X, .(H, M))
U6_gaaa(T, Y, Xs, Ts, R, Rs, EvenOdd, last_out_gaa(.(Y, Xs), R, Rests)) → U7_gaaa(T, Y, Xs, Ts, R, Rs, EvenOdd, halves_in_gaaa(Rests, Ts, Rs, EvenOdd))
U7_gaaa(T, Y, Xs, Ts, R, Rs, EvenOdd, halves_out_gaaa(Rests, Ts, Rs, EvenOdd)) → halves_out_gaaa(.(T, .(Y, Xs)), .(T, Ts), .(R, Rs), EvenOdd)
U1_g(L, halves_out_gaaa(L, X1s, X2s, EvenOdd)) → U2_g(L, X1s, X2s, eq_in_gg(EvenOdd, even))
eq_in_gg(X, X) → eq_out_gg(X, X)
U2_g(L, X1s, X2s, eq_out_gg(EvenOdd, even)) → U3_g(L, eq_in_gg(X1s, X2s))
U3_g(L, eq_out_gg(X1s, X2s)) → palindrome_out_g(L)
U1_g(L, halves_out_gaaa(L, X1s, X2s, EvenOdd)) → U4_g(L, X1s, X2s, eq_in_gg(EvenOdd, odd))
U4_g(L, X1s, X2s, eq_out_gg(EvenOdd, odd)) → U5_g(L, last_in_gag(X1s, X1, X2s))
last_in_gag(.(T, []), T, []) → last_out_gag(.(T, []), T, [])
last_in_gag(.(H, T), X, .(H, M)) → U8_gag(H, T, X, M, last_in_gag(T, X, M))
U8_gag(H, T, X, M, last_out_gag(T, X, M)) → last_out_gag(.(H, T), X, .(H, M))
U5_g(L, last_out_gag(X1s, X1, X2s)) → palindrome_out_g(L)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
palindrome_in_g(L) → U1_g(L, halves_in_gaaa(L, X1s, X2s, EvenOdd))
halves_in_gaaa([], [], [], even) → halves_out_gaaa([], [], [], even)
halves_in_gaaa(.(X, []), .(X, []), [], odd) → halves_out_gaaa(.(X, []), .(X, []), [], odd)
halves_in_gaaa(.(T, .(Y, Xs)), .(T, Ts), .(R, Rs), EvenOdd) → U6_gaaa(T, Y, Xs, Ts, R, Rs, EvenOdd, last_in_gaa(.(Y, Xs), R, Rests))
last_in_gaa(.(T, []), T, []) → last_out_gaa(.(T, []), T, [])
last_in_gaa(.(H, T), X, .(H, M)) → U8_gaa(H, T, X, M, last_in_gaa(T, X, M))
U8_gaa(H, T, X, M, last_out_gaa(T, X, M)) → last_out_gaa(.(H, T), X, .(H, M))
U6_gaaa(T, Y, Xs, Ts, R, Rs, EvenOdd, last_out_gaa(.(Y, Xs), R, Rests)) → U7_gaaa(T, Y, Xs, Ts, R, Rs, EvenOdd, halves_in_gaaa(Rests, Ts, Rs, EvenOdd))
U7_gaaa(T, Y, Xs, Ts, R, Rs, EvenOdd, halves_out_gaaa(Rests, Ts, Rs, EvenOdd)) → halves_out_gaaa(.(T, .(Y, Xs)), .(T, Ts), .(R, Rs), EvenOdd)
U1_g(L, halves_out_gaaa(L, X1s, X2s, EvenOdd)) → U2_g(L, X1s, X2s, eq_in_gg(EvenOdd, even))
eq_in_gg(X, X) → eq_out_gg(X, X)
U2_g(L, X1s, X2s, eq_out_gg(EvenOdd, even)) → U3_g(L, eq_in_gg(X1s, X2s))
U3_g(L, eq_out_gg(X1s, X2s)) → palindrome_out_g(L)
U1_g(L, halves_out_gaaa(L, X1s, X2s, EvenOdd)) → U4_g(L, X1s, X2s, eq_in_gg(EvenOdd, odd))
U4_g(L, X1s, X2s, eq_out_gg(EvenOdd, odd)) → U5_g(L, last_in_gag(X1s, X1, X2s))
last_in_gag(.(T, []), T, []) → last_out_gag(.(T, []), T, [])
last_in_gag(.(H, T), X, .(H, M)) → U8_gag(H, T, X, M, last_in_gag(T, X, M))
U8_gag(H, T, X, M, last_out_gag(T, X, M)) → last_out_gag(.(H, T), X, .(H, M))
U5_g(L, last_out_gag(X1s, X1, X2s)) → palindrome_out_g(L)
PALINDROME_IN_G(L) → U1_G(L, halves_in_gaaa(L, X1s, X2s, EvenOdd))
PALINDROME_IN_G(L) → HALVES_IN_GAAA(L, X1s, X2s, EvenOdd)
HALVES_IN_GAAA(.(T, .(Y, Xs)), .(T, Ts), .(R, Rs), EvenOdd) → U6_GAAA(T, Y, Xs, Ts, R, Rs, EvenOdd, last_in_gaa(.(Y, Xs), R, Rests))
HALVES_IN_GAAA(.(T, .(Y, Xs)), .(T, Ts), .(R, Rs), EvenOdd) → LAST_IN_GAA(.(Y, Xs), R, Rests)
LAST_IN_GAA(.(H, T), X, .(H, M)) → U8_GAA(H, T, X, M, last_in_gaa(T, X, M))
LAST_IN_GAA(.(H, T), X, .(H, M)) → LAST_IN_GAA(T, X, M)
U6_GAAA(T, Y, Xs, Ts, R, Rs, EvenOdd, last_out_gaa(.(Y, Xs), R, Rests)) → U7_GAAA(T, Y, Xs, Ts, R, Rs, EvenOdd, halves_in_gaaa(Rests, Ts, Rs, EvenOdd))
U6_GAAA(T, Y, Xs, Ts, R, Rs, EvenOdd, last_out_gaa(.(Y, Xs), R, Rests)) → HALVES_IN_GAAA(Rests, Ts, Rs, EvenOdd)
U1_G(L, halves_out_gaaa(L, X1s, X2s, EvenOdd)) → U2_G(L, X1s, X2s, eq_in_gg(EvenOdd, even))
U1_G(L, halves_out_gaaa(L, X1s, X2s, EvenOdd)) → EQ_IN_GG(EvenOdd, even)
U2_G(L, X1s, X2s, eq_out_gg(EvenOdd, even)) → U3_G(L, eq_in_gg(X1s, X2s))
U2_G(L, X1s, X2s, eq_out_gg(EvenOdd, even)) → EQ_IN_GG(X1s, X2s)
U1_G(L, halves_out_gaaa(L, X1s, X2s, EvenOdd)) → U4_G(L, X1s, X2s, eq_in_gg(EvenOdd, odd))
U1_G(L, halves_out_gaaa(L, X1s, X2s, EvenOdd)) → EQ_IN_GG(EvenOdd, odd)
U4_G(L, X1s, X2s, eq_out_gg(EvenOdd, odd)) → U5_G(L, last_in_gag(X1s, X1, X2s))
U4_G(L, X1s, X2s, eq_out_gg(EvenOdd, odd)) → LAST_IN_GAG(X1s, X1, X2s)
LAST_IN_GAG(.(H, T), X, .(H, M)) → U8_GAG(H, T, X, M, last_in_gag(T, X, M))
LAST_IN_GAG(.(H, T), X, .(H, M)) → LAST_IN_GAG(T, X, M)
palindrome_in_g(L) → U1_g(L, halves_in_gaaa(L, X1s, X2s, EvenOdd))
halves_in_gaaa([], [], [], even) → halves_out_gaaa([], [], [], even)
halves_in_gaaa(.(X, []), .(X, []), [], odd) → halves_out_gaaa(.(X, []), .(X, []), [], odd)
halves_in_gaaa(.(T, .(Y, Xs)), .(T, Ts), .(R, Rs), EvenOdd) → U6_gaaa(T, Y, Xs, Ts, R, Rs, EvenOdd, last_in_gaa(.(Y, Xs), R, Rests))
last_in_gaa(.(T, []), T, []) → last_out_gaa(.(T, []), T, [])
last_in_gaa(.(H, T), X, .(H, M)) → U8_gaa(H, T, X, M, last_in_gaa(T, X, M))
U8_gaa(H, T, X, M, last_out_gaa(T, X, M)) → last_out_gaa(.(H, T), X, .(H, M))
U6_gaaa(T, Y, Xs, Ts, R, Rs, EvenOdd, last_out_gaa(.(Y, Xs), R, Rests)) → U7_gaaa(T, Y, Xs, Ts, R, Rs, EvenOdd, halves_in_gaaa(Rests, Ts, Rs, EvenOdd))
U7_gaaa(T, Y, Xs, Ts, R, Rs, EvenOdd, halves_out_gaaa(Rests, Ts, Rs, EvenOdd)) → halves_out_gaaa(.(T, .(Y, Xs)), .(T, Ts), .(R, Rs), EvenOdd)
U1_g(L, halves_out_gaaa(L, X1s, X2s, EvenOdd)) → U2_g(L, X1s, X2s, eq_in_gg(EvenOdd, even))
eq_in_gg(X, X) → eq_out_gg(X, X)
U2_g(L, X1s, X2s, eq_out_gg(EvenOdd, even)) → U3_g(L, eq_in_gg(X1s, X2s))
U3_g(L, eq_out_gg(X1s, X2s)) → palindrome_out_g(L)
U1_g(L, halves_out_gaaa(L, X1s, X2s, EvenOdd)) → U4_g(L, X1s, X2s, eq_in_gg(EvenOdd, odd))
U4_g(L, X1s, X2s, eq_out_gg(EvenOdd, odd)) → U5_g(L, last_in_gag(X1s, X1, X2s))
last_in_gag(.(T, []), T, []) → last_out_gag(.(T, []), T, [])
last_in_gag(.(H, T), X, .(H, M)) → U8_gag(H, T, X, M, last_in_gag(T, X, M))
U8_gag(H, T, X, M, last_out_gag(T, X, M)) → last_out_gag(.(H, T), X, .(H, M))
U5_g(L, last_out_gag(X1s, X1, X2s)) → palindrome_out_g(L)
PALINDROME_IN_G(L) → U1_G(L, halves_in_gaaa(L, X1s, X2s, EvenOdd))
PALINDROME_IN_G(L) → HALVES_IN_GAAA(L, X1s, X2s, EvenOdd)
HALVES_IN_GAAA(.(T, .(Y, Xs)), .(T, Ts), .(R, Rs), EvenOdd) → U6_GAAA(T, Y, Xs, Ts, R, Rs, EvenOdd, last_in_gaa(.(Y, Xs), R, Rests))
HALVES_IN_GAAA(.(T, .(Y, Xs)), .(T, Ts), .(R, Rs), EvenOdd) → LAST_IN_GAA(.(Y, Xs), R, Rests)
LAST_IN_GAA(.(H, T), X, .(H, M)) → U8_GAA(H, T, X, M, last_in_gaa(T, X, M))
LAST_IN_GAA(.(H, T), X, .(H, M)) → LAST_IN_GAA(T, X, M)
U6_GAAA(T, Y, Xs, Ts, R, Rs, EvenOdd, last_out_gaa(.(Y, Xs), R, Rests)) → U7_GAAA(T, Y, Xs, Ts, R, Rs, EvenOdd, halves_in_gaaa(Rests, Ts, Rs, EvenOdd))
U6_GAAA(T, Y, Xs, Ts, R, Rs, EvenOdd, last_out_gaa(.(Y, Xs), R, Rests)) → HALVES_IN_GAAA(Rests, Ts, Rs, EvenOdd)
U1_G(L, halves_out_gaaa(L, X1s, X2s, EvenOdd)) → U2_G(L, X1s, X2s, eq_in_gg(EvenOdd, even))
U1_G(L, halves_out_gaaa(L, X1s, X2s, EvenOdd)) → EQ_IN_GG(EvenOdd, even)
U2_G(L, X1s, X2s, eq_out_gg(EvenOdd, even)) → U3_G(L, eq_in_gg(X1s, X2s))
U2_G(L, X1s, X2s, eq_out_gg(EvenOdd, even)) → EQ_IN_GG(X1s, X2s)
U1_G(L, halves_out_gaaa(L, X1s, X2s, EvenOdd)) → U4_G(L, X1s, X2s, eq_in_gg(EvenOdd, odd))
U1_G(L, halves_out_gaaa(L, X1s, X2s, EvenOdd)) → EQ_IN_GG(EvenOdd, odd)
U4_G(L, X1s, X2s, eq_out_gg(EvenOdd, odd)) → U5_G(L, last_in_gag(X1s, X1, X2s))
U4_G(L, X1s, X2s, eq_out_gg(EvenOdd, odd)) → LAST_IN_GAG(X1s, X1, X2s)
LAST_IN_GAG(.(H, T), X, .(H, M)) → U8_GAG(H, T, X, M, last_in_gag(T, X, M))
LAST_IN_GAG(.(H, T), X, .(H, M)) → LAST_IN_GAG(T, X, M)
palindrome_in_g(L) → U1_g(L, halves_in_gaaa(L, X1s, X2s, EvenOdd))
halves_in_gaaa([], [], [], even) → halves_out_gaaa([], [], [], even)
halves_in_gaaa(.(X, []), .(X, []), [], odd) → halves_out_gaaa(.(X, []), .(X, []), [], odd)
halves_in_gaaa(.(T, .(Y, Xs)), .(T, Ts), .(R, Rs), EvenOdd) → U6_gaaa(T, Y, Xs, Ts, R, Rs, EvenOdd, last_in_gaa(.(Y, Xs), R, Rests))
last_in_gaa(.(T, []), T, []) → last_out_gaa(.(T, []), T, [])
last_in_gaa(.(H, T), X, .(H, M)) → U8_gaa(H, T, X, M, last_in_gaa(T, X, M))
U8_gaa(H, T, X, M, last_out_gaa(T, X, M)) → last_out_gaa(.(H, T), X, .(H, M))
U6_gaaa(T, Y, Xs, Ts, R, Rs, EvenOdd, last_out_gaa(.(Y, Xs), R, Rests)) → U7_gaaa(T, Y, Xs, Ts, R, Rs, EvenOdd, halves_in_gaaa(Rests, Ts, Rs, EvenOdd))
U7_gaaa(T, Y, Xs, Ts, R, Rs, EvenOdd, halves_out_gaaa(Rests, Ts, Rs, EvenOdd)) → halves_out_gaaa(.(T, .(Y, Xs)), .(T, Ts), .(R, Rs), EvenOdd)
U1_g(L, halves_out_gaaa(L, X1s, X2s, EvenOdd)) → U2_g(L, X1s, X2s, eq_in_gg(EvenOdd, even))
eq_in_gg(X, X) → eq_out_gg(X, X)
U2_g(L, X1s, X2s, eq_out_gg(EvenOdd, even)) → U3_g(L, eq_in_gg(X1s, X2s))
U3_g(L, eq_out_gg(X1s, X2s)) → palindrome_out_g(L)
U1_g(L, halves_out_gaaa(L, X1s, X2s, EvenOdd)) → U4_g(L, X1s, X2s, eq_in_gg(EvenOdd, odd))
U4_g(L, X1s, X2s, eq_out_gg(EvenOdd, odd)) → U5_g(L, last_in_gag(X1s, X1, X2s))
last_in_gag(.(T, []), T, []) → last_out_gag(.(T, []), T, [])
last_in_gag(.(H, T), X, .(H, M)) → U8_gag(H, T, X, M, last_in_gag(T, X, M))
U8_gag(H, T, X, M, last_out_gag(T, X, M)) → last_out_gag(.(H, T), X, .(H, M))
U5_g(L, last_out_gag(X1s, X1, X2s)) → palindrome_out_g(L)
LAST_IN_GAG(.(H, T), X, .(H, M)) → LAST_IN_GAG(T, X, M)
palindrome_in_g(L) → U1_g(L, halves_in_gaaa(L, X1s, X2s, EvenOdd))
halves_in_gaaa([], [], [], even) → halves_out_gaaa([], [], [], even)
halves_in_gaaa(.(X, []), .(X, []), [], odd) → halves_out_gaaa(.(X, []), .(X, []), [], odd)
halves_in_gaaa(.(T, .(Y, Xs)), .(T, Ts), .(R, Rs), EvenOdd) → U6_gaaa(T, Y, Xs, Ts, R, Rs, EvenOdd, last_in_gaa(.(Y, Xs), R, Rests))
last_in_gaa(.(T, []), T, []) → last_out_gaa(.(T, []), T, [])
last_in_gaa(.(H, T), X, .(H, M)) → U8_gaa(H, T, X, M, last_in_gaa(T, X, M))
U8_gaa(H, T, X, M, last_out_gaa(T, X, M)) → last_out_gaa(.(H, T), X, .(H, M))
U6_gaaa(T, Y, Xs, Ts, R, Rs, EvenOdd, last_out_gaa(.(Y, Xs), R, Rests)) → U7_gaaa(T, Y, Xs, Ts, R, Rs, EvenOdd, halves_in_gaaa(Rests, Ts, Rs, EvenOdd))
U7_gaaa(T, Y, Xs, Ts, R, Rs, EvenOdd, halves_out_gaaa(Rests, Ts, Rs, EvenOdd)) → halves_out_gaaa(.(T, .(Y, Xs)), .(T, Ts), .(R, Rs), EvenOdd)
U1_g(L, halves_out_gaaa(L, X1s, X2s, EvenOdd)) → U2_g(L, X1s, X2s, eq_in_gg(EvenOdd, even))
eq_in_gg(X, X) → eq_out_gg(X, X)
U2_g(L, X1s, X2s, eq_out_gg(EvenOdd, even)) → U3_g(L, eq_in_gg(X1s, X2s))
U3_g(L, eq_out_gg(X1s, X2s)) → palindrome_out_g(L)
U1_g(L, halves_out_gaaa(L, X1s, X2s, EvenOdd)) → U4_g(L, X1s, X2s, eq_in_gg(EvenOdd, odd))
U4_g(L, X1s, X2s, eq_out_gg(EvenOdd, odd)) → U5_g(L, last_in_gag(X1s, X1, X2s))
last_in_gag(.(T, []), T, []) → last_out_gag(.(T, []), T, [])
last_in_gag(.(H, T), X, .(H, M)) → U8_gag(H, T, X, M, last_in_gag(T, X, M))
U8_gag(H, T, X, M, last_out_gag(T, X, M)) → last_out_gag(.(H, T), X, .(H, M))
U5_g(L, last_out_gag(X1s, X1, X2s)) → palindrome_out_g(L)
LAST_IN_GAG(.(H, T), X, .(H, M)) → LAST_IN_GAG(T, X, M)
LAST_IN_GAG(.(H, T), .(H, M)) → LAST_IN_GAG(T, M)
From the DPs we obtained the following set of size-change graphs:
LAST_IN_GAA(.(H, T), X, .(H, M)) → LAST_IN_GAA(T, X, M)
palindrome_in_g(L) → U1_g(L, halves_in_gaaa(L, X1s, X2s, EvenOdd))
halves_in_gaaa([], [], [], even) → halves_out_gaaa([], [], [], even)
halves_in_gaaa(.(X, []), .(X, []), [], odd) → halves_out_gaaa(.(X, []), .(X, []), [], odd)
halves_in_gaaa(.(T, .(Y, Xs)), .(T, Ts), .(R, Rs), EvenOdd) → U6_gaaa(T, Y, Xs, Ts, R, Rs, EvenOdd, last_in_gaa(.(Y, Xs), R, Rests))
last_in_gaa(.(T, []), T, []) → last_out_gaa(.(T, []), T, [])
last_in_gaa(.(H, T), X, .(H, M)) → U8_gaa(H, T, X, M, last_in_gaa(T, X, M))
U8_gaa(H, T, X, M, last_out_gaa(T, X, M)) → last_out_gaa(.(H, T), X, .(H, M))
U6_gaaa(T, Y, Xs, Ts, R, Rs, EvenOdd, last_out_gaa(.(Y, Xs), R, Rests)) → U7_gaaa(T, Y, Xs, Ts, R, Rs, EvenOdd, halves_in_gaaa(Rests, Ts, Rs, EvenOdd))
U7_gaaa(T, Y, Xs, Ts, R, Rs, EvenOdd, halves_out_gaaa(Rests, Ts, Rs, EvenOdd)) → halves_out_gaaa(.(T, .(Y, Xs)), .(T, Ts), .(R, Rs), EvenOdd)
U1_g(L, halves_out_gaaa(L, X1s, X2s, EvenOdd)) → U2_g(L, X1s, X2s, eq_in_gg(EvenOdd, even))
eq_in_gg(X, X) → eq_out_gg(X, X)
U2_g(L, X1s, X2s, eq_out_gg(EvenOdd, even)) → U3_g(L, eq_in_gg(X1s, X2s))
U3_g(L, eq_out_gg(X1s, X2s)) → palindrome_out_g(L)
U1_g(L, halves_out_gaaa(L, X1s, X2s, EvenOdd)) → U4_g(L, X1s, X2s, eq_in_gg(EvenOdd, odd))
U4_g(L, X1s, X2s, eq_out_gg(EvenOdd, odd)) → U5_g(L, last_in_gag(X1s, X1, X2s))
last_in_gag(.(T, []), T, []) → last_out_gag(.(T, []), T, [])
last_in_gag(.(H, T), X, .(H, M)) → U8_gag(H, T, X, M, last_in_gag(T, X, M))
U8_gag(H, T, X, M, last_out_gag(T, X, M)) → last_out_gag(.(H, T), X, .(H, M))
U5_g(L, last_out_gag(X1s, X1, X2s)) → palindrome_out_g(L)
LAST_IN_GAA(.(H, T), X, .(H, M)) → LAST_IN_GAA(T, X, M)
LAST_IN_GAA(.(H, T)) → LAST_IN_GAA(T)
From the DPs we obtained the following set of size-change graphs:
U6_GAAA(T, Y, Xs, Ts, R, Rs, EvenOdd, last_out_gaa(.(Y, Xs), R, Rests)) → HALVES_IN_GAAA(Rests, Ts, Rs, EvenOdd)
HALVES_IN_GAAA(.(T, .(Y, Xs)), .(T, Ts), .(R, Rs), EvenOdd) → U6_GAAA(T, Y, Xs, Ts, R, Rs, EvenOdd, last_in_gaa(.(Y, Xs), R, Rests))
palindrome_in_g(L) → U1_g(L, halves_in_gaaa(L, X1s, X2s, EvenOdd))
halves_in_gaaa([], [], [], even) → halves_out_gaaa([], [], [], even)
halves_in_gaaa(.(X, []), .(X, []), [], odd) → halves_out_gaaa(.(X, []), .(X, []), [], odd)
halves_in_gaaa(.(T, .(Y, Xs)), .(T, Ts), .(R, Rs), EvenOdd) → U6_gaaa(T, Y, Xs, Ts, R, Rs, EvenOdd, last_in_gaa(.(Y, Xs), R, Rests))
last_in_gaa(.(T, []), T, []) → last_out_gaa(.(T, []), T, [])
last_in_gaa(.(H, T), X, .(H, M)) → U8_gaa(H, T, X, M, last_in_gaa(T, X, M))
U8_gaa(H, T, X, M, last_out_gaa(T, X, M)) → last_out_gaa(.(H, T), X, .(H, M))
U6_gaaa(T, Y, Xs, Ts, R, Rs, EvenOdd, last_out_gaa(.(Y, Xs), R, Rests)) → U7_gaaa(T, Y, Xs, Ts, R, Rs, EvenOdd, halves_in_gaaa(Rests, Ts, Rs, EvenOdd))
U7_gaaa(T, Y, Xs, Ts, R, Rs, EvenOdd, halves_out_gaaa(Rests, Ts, Rs, EvenOdd)) → halves_out_gaaa(.(T, .(Y, Xs)), .(T, Ts), .(R, Rs), EvenOdd)
U1_g(L, halves_out_gaaa(L, X1s, X2s, EvenOdd)) → U2_g(L, X1s, X2s, eq_in_gg(EvenOdd, even))
eq_in_gg(X, X) → eq_out_gg(X, X)
U2_g(L, X1s, X2s, eq_out_gg(EvenOdd, even)) → U3_g(L, eq_in_gg(X1s, X2s))
U3_g(L, eq_out_gg(X1s, X2s)) → palindrome_out_g(L)
U1_g(L, halves_out_gaaa(L, X1s, X2s, EvenOdd)) → U4_g(L, X1s, X2s, eq_in_gg(EvenOdd, odd))
U4_g(L, X1s, X2s, eq_out_gg(EvenOdd, odd)) → U5_g(L, last_in_gag(X1s, X1, X2s))
last_in_gag(.(T, []), T, []) → last_out_gag(.(T, []), T, [])
last_in_gag(.(H, T), X, .(H, M)) → U8_gag(H, T, X, M, last_in_gag(T, X, M))
U8_gag(H, T, X, M, last_out_gag(T, X, M)) → last_out_gag(.(H, T), X, .(H, M))
U5_g(L, last_out_gag(X1s, X1, X2s)) → palindrome_out_g(L)
U6_GAAA(T, Y, Xs, Ts, R, Rs, EvenOdd, last_out_gaa(.(Y, Xs), R, Rests)) → HALVES_IN_GAAA(Rests, Ts, Rs, EvenOdd)
HALVES_IN_GAAA(.(T, .(Y, Xs)), .(T, Ts), .(R, Rs), EvenOdd) → U6_GAAA(T, Y, Xs, Ts, R, Rs, EvenOdd, last_in_gaa(.(Y, Xs), R, Rests))
last_in_gaa(.(T, []), T, []) → last_out_gaa(.(T, []), T, [])
last_in_gaa(.(H, T), X, .(H, M)) → U8_gaa(H, T, X, M, last_in_gaa(T, X, M))
U8_gaa(H, T, X, M, last_out_gaa(T, X, M)) → last_out_gaa(.(H, T), X, .(H, M))
U6_GAAA(T, last_out_gaa(R, Rests)) → HALVES_IN_GAAA(Rests)
HALVES_IN_GAAA(.(T, .(Y, Xs))) → U6_GAAA(T, last_in_gaa(.(Y, Xs)))
last_in_gaa(.(T, [])) → last_out_gaa(T, [])
last_in_gaa(.(H, T)) → U8_gaa(H, last_in_gaa(T))
U8_gaa(H, last_out_gaa(X, M)) → last_out_gaa(X, .(H, M))
last_in_gaa(x0)
U8_gaa(x0, x1)
U6_GAAA(T, last_out_gaa(R, Rests)) → HALVES_IN_GAAA(Rests)
HALVES_IN_GAAA(.(T, .(Y, Xs))) → U6_GAAA(T, last_in_gaa(.(Y, Xs)))
last_in_gaa(.(T, [])) → last_out_gaa(T, [])
last_in_gaa(.(H, T)) → U8_gaa(H, last_in_gaa(T))
U8_gaa(H, last_out_gaa(X, M)) → last_out_gaa(X, .(H, M))
U6GAAA2 > lastingaa1 > U8gaa2 > HALVESINGAAA1 > .2 > lastoutgaa2 > []
[]=1
last_in_gaa_1=1
HALVES_IN_GAAA_1=2
._2=0
last_out_gaa_2=1
U8_gaa_2=0
U6_GAAA_2=0
last_in_gaa(x0)
U8_gaa(x0, x1)